Martin-Löf’s type theory differs from other systems of logic in several respects. One respect is the way in which identity is treated. I will give an introduction to this topic, presupposing no familiarity with Martin-Löf’s type theory. Throughout I will emphasize the motivation for the various at first perhaps unfamiliar ideas. In particular I will spend much time on the distinction between judgemental and propositional identity and on the introduction and elimination rules for the latter.